\documentclass{beamer}
\usepackage[tight]{k-beamer}
\usepackage{beamerthemeBoadilla} %// Activate for custom appearance
%\usepackage{Singapore}
\usepackage{multirow}

\newcommand{\htriple}[3]{\{{#1}\}{#2}\{{#3}\}}


\title{Engineering Hoare-Logic based\\Program Verification in \K}
\author{Andrei Arusoaie}
\institute[UAIC]{Faculty of Computer Science, Ia\c{s}i\\~\\SYNASC 2013}
\date{\today}

\begin{document}

\frame{\titlepage}

\section[Outline]{}
\frame{\tableofcontents}

\section{Motivation}
\frame{
  \frametitle{Motivation}
  \begin{itemize}
  \item<1-> \K - (remember Grigore Ro\c{s}u's talk)
  \item<1-> Framework for defining operational semantics of programming languages (PL)
  \item<2-> We are interested in using the \K semantics for program verification 
%  \item<3-> We want a language independent framework which provides support for verification
  \item<3-> Reachability Logic (see MatchC approach)
  \item<4-> What about Hoare Logic?
  \end{itemize}
}

\frame{
  \frametitle{Motivation}
  \begin{itemize}
%  \item<1-> Hoare triples $\to$ Reachability formulas
%  \begin{thebibliography}{1}
%\bibitem{rosu-stefanescu-2012-fm}
%Grigore Ro\c{s}u and Andrei \c{S}tef\u{a}nescu.
%\newblock From hoare logic to matching logic reachability.
%\newblock FM'12
%\end{thebibliography}
  \item<1-> What should we do (in practice) to a create a Hoare-like verifier using the \K semantics of a PL?
  \end{itemize}
}

%\section{Problem description}
\frame{
  \frametitle{Problem}
  \begin{itemize}
  \item<1-> Given $\cal{S}$, the \K semantics of a programming language $\cal{L}$
  \item<2-> Provide a methodology, which applied to the semantics of \cal{L} transforms the \K tool into a Hoare-like verification tool
  \end{itemize}
}


\section{\K}
%\subsection{The \K Framework}
\frame{
	\frametitle{\K  - remember Grigore Ro\c{s}u's talk}
	\begin{itemize}
	\item \K - framework for defining operational semantics of programming languages
	\end{itemize}
	\begin{itemize}
	\item<1> Imperative: IMP, SIMPLE (untyped, typed), {\textbf{C}}
	\item<1> Object Oriented: KOOL (untyped, typed), {\textbf{Java}}, {\textbf{Python}}
	\item<1> Assembly: SSRISC, Verilog
	\item<1> Functional: Scheme, Haskell, OCaml
%	\item<1> In progress: JavaScript, LLVM, ...
	\end{itemize}
}

\frame{
	\frametitle{Defining languages in \K}
	\begin{enumerate}
	\item<1-> Define $\cal{L}$'s syntax (BNF)
	\item<2-> Define $\cal{L}$'s semantics
	\begin{enumerate}
	\item configuration - nested structure of cells
	\item {\it k} - computations cell
	\item \K rules - rewriting rules
	\end{enumerate}
	\end{enumerate}
}


%\subsection{Example}
\frame{
  \frametitle{IMP syntax}
\begin{itemize}
\item<1-> IMP statements
%\begin{minipage}{.9\linewidth}
%\small
%\begin{syntaxBlock}{\nonTerminal{\sort{AExp}}}\syntax{{\nonTerminal{\sort{Int} $\mid$ \sort{Id}}}}{}
%\syntaxCont{{{\nonTerminal{\sort{AExp}}}}\terminal{/}{{\nonTerminal{\sort{AExp}}}}}{\kattribute{strict}}
%\syntaxCont{{{\nonTerminal{\sort{AExp}}}}\terminal{+}{{\nonTerminal{\sort{AExp}}}}}{\kattribute{strict}}
%\syntaxCont{({{\nonTerminal{\sort{AExp}}}})}{\kattribute{bracket}}
%\end{syntaxBlock}
%\vspace*{-3ex}
%\begin{syntaxBlock}{\nonTerminal{\sort{BExp}}}\syntax{{\nonTerminal{\sort{Bool}}}}{}\syntaxCont{{{\nonTerminal{\sort{AExp}}}}\leq{{\nonTerminal{\sort{AExp}}}}}{\kattribute{seqstrict}}\syntaxCont{{}\terminal{!}{{\nonTerminal{\sort{BExp}}}}}{\kattribute{strict}}\syntaxCont{{{\nonTerminal{\sort{BExp}}}}\terminal{\&\&}{{\nonTerminal{\sort{BExp}}}}}{\kattribute{strict}(1)}\syntaxCont{({{\nonTerminal{\sort{BExp}}}})}{\kattribute{bracket}}
%\end{syntaxBlock}
%\vspace*{-2.8ex}
%\begin{syntaxBlock}{\nonTerminal{\sort{Block}}}\syntax{\{\} \mid \{{{\nonTerminal{\sort{Stmt}}}}\}  }{}
%\end{syntaxBlock}
%\vspace*{2ex}
\begin{syntaxBlock}{\nonTerminal{\sort{Stmt}}}\syntax{\{\} \mid \{{{\nonTerminal{\sort{Stmt}}}}\}  }{}\syntaxCont{{{\nonTerminal{\sort{Id}}}}\terminal{=}{{\nonTerminal{\sort{AExp}}}}\terminal{;}}{\kattribute{strict}(2)}\syntaxCont{{}\terminal{if}({{\nonTerminal{\sort{BExp}}}}){{\nonTerminal{\sort{Block}}}}\terminal{else}{{\nonTerminal{\sort{Block}}}}}{\kattribute{strict}(1)}\syntaxCont{{}\terminal{while}({{\nonTerminal{\sort{BExp}}}}){{\nonTerminal{\sort{Block}}}}}{}\syntaxCont{{{\nonTerminal{\sort{Stmt}}}}\mathrel{}{{\nonTerminal{\sort{Stmt}}}}}{}
\end{syntaxBlock}
%\vspace*{-3ex}
%\begin{syntaxBlock}{\nonTerminal{\sort{Pgm}}}\syntax{{}\terminal{int}{{\nonTerminal{\sort{Ids}}}}\terminal{;}{{\nonTerminal{\sort{Stmt}}}}}{}
%\end{syntaxBlock}
%\vspace*{-3ex}
%\begin{syntaxBlock}{\nonTerminal{\sort{Ids}}}\syntax{List\{{\nonTerminal{\sort{Id}}}, \mbox{``},\mbox{''}\}}{}
%\end{syntaxBlock}
%\end{minipage}
\item<2-> Sample program \texttt{SUM}:\\

\hspace{22ex}\begin{minipage}{.6\linewidth}
\texttt{S = 0; i = 1;\\ while(i <= n) \{\\\hspace*{3ex}S = S + i;\\\hspace*{3ex}i = i + 1;\\\}\\}
\end{minipage}
\end{itemize}
}

\frame{
  \frametitle{IMP configuration}
  
\begin{itemize}[]
\item[]<1-> IMP configuration:
$${\kall[green]{T}{\kall[blue]{k}{\variable[Pgm]{Pgm}}
\mathrel{}\kall[yellow]{state}{Map_{Id, Int}}
}}$$

\item[]<2-> Concrete configuration:\\

\hspace*{5ex}$\kall[blue]{k}{\variable[Pgm]{\texttt{S=0; i=1; while(i<=n)\{ S=S+i; i=i+1;\}}}}$\\
\hspace*{4.5ex}$\mathrel{}\kall[yellow]{state}{\texttt{S} \mapsto 0~\texttt{i} \mapsto 0~\texttt{n} \mapsto 10}$

%\item[]<3-> Assignment:\\
%\hspace*{10ex}
%${
%\kprefix[blue]{k}{\reduce{{\variable[K]{X}}\terminal{=}{\variable[Int]{I}}\terminal{;}}{\dotCt{K}}}
%\mathrel{}\kmiddle[yellow]{state}{\variable[K]{X}\mapsto\reduce{\AnyVar[K]}{\variable[Int]{I}}}
%}{}{}{}{}
%$
%\item[]<4-> Concrete configuration:
%\hspace*{5ex}$\kall[blue]{k}{\variable[Pgm]{\texttt{{\color{red}{S=0;}} i=1; while(i<=n)\{ S=S+i; i=i+1;\}}}}$\\
%\hspace*{5ex}$\mathrel{}\kall[yellow]{state}{{\color{red}{\texttt{S} \mapsto 0}}~\texttt{i} \mapsto 0~\texttt{n} \mapsto 10}$
\end{itemize}
}

\frame{
  \frametitle{IMP semantics}
  \begin{itemize}
\item[]<1-> Assignment:\\
\hspace*{10ex}
${
\kprefix[blue]{k}{\reduce{{\variable[K]{X}}\terminal{=}{\variable[Int]{I}}\terminal{;}}{\dotCt{K}}}
\mathrel{}\kmiddle[yellow]{state}{\variable[K]{X}\mapsto\reduce{\AnyVar[K]}{\variable[Int]{I}}}
}{}{}{}{}
$
\item[]<2-> Concrete configuration:\\
\hspace*{5ex}$\kall[blue]{k}{\variable[Pgm]{\texttt{{\color{black}{S=0;}} i=1; while(i<=n)\{ S=S+i; i=i+1;\}}}}$\\
\hspace*{5ex}$\mathrel{}\kall[yellow]{state}{{\color{black}{\texttt{S} \mapsto 0}}~\texttt{i} \mapsto 0~\texttt{n} \mapsto 10}$
\end{itemize}
}

\frame{
  \frametitle{IMP semantics}
  \begin{itemize}
\item[] Assignment:\\
\hspace*{10ex}
${
\kprefix[blue]{k}{\reduce{{\color{blue}{\variable[K]{X}}}\terminal{=}{{\color{red}{\variable[Int]{I}}}}\terminal{;}}{\dotCt{K}}}
\mathrel{}\kmiddle[yellow]{state}{{\color{blue}{\variable[K]{X}}}\mapsto\reduce{{\color{green}{\AnyVar[K]}}}{\variable[Int]{{\color{red}{I}}}}}
}{}{}{}{}
$
\item[] Concrete configuration:\\
\hspace*{5ex}$\kall[blue]{k}{\variable[Pgm]{\texttt{{\color{blue}{S}}={\color{red}{0}}; i=1; while(i<=n)\{ S=S+i; i=i+1;\}}}}$\\
\hspace*{5ex}$\mathrel{}\kall[yellow]{state}{{\color{blue}{\texttt{S}}} \mapsto {\color{green}{0}}~\texttt{i} \mapsto 0~\texttt{n} \mapsto 10}$
\end{itemize}
}

\frame{
  \frametitle{IMP semantics}
  \begin{itemize}
\item[] Assignment:\\
\hspace*{10ex}
${
\kprefix[blue]{k}{\reduce{{\variable[K]{X}}\terminal{=}{\variable[Int]{I}}\terminal{;}}{\dotCt{K}}}
\mathrel{}\kmiddle[yellow]{state}{\variable[K]{X}\mapsto\reduce{\AnyVar[K]}{\variable[Int]{I}}}
}{}{}{}{}
$
\item[] Concrete configuration:\\
\hspace*{5ex}$\kall[blue]{k}{\variable[Pgm]{\texttt{i=1; while(i<=n)\{ S=S+i; i=i+1;\}}}}$\\
\hspace*{5ex}$\mathrel{}\kall[yellow]{state}{\texttt{S} \mapsto {\color{red}{0}}~\texttt{i} \mapsto 0~\texttt{n} \mapsto 10}$
\end{itemize}
}

\frame{
  \frametitle{IMP semantics}
  \begin{itemize}
\item[] Assignment:\\
\hspace*{10ex}
${
\kprefix[blue]{k}{\reduce{{\color{blue}{\variable[K]{X}}}\terminal{=}{{\color{red}{\variable[Int]{I}}}}\terminal{;}}{\dotCt{K}}}
\mathrel{}\kmiddle[yellow]{state}{{\color{blue}{\variable[K]{X}}}\mapsto\reduce{{\color{green}{\AnyVar[K]}}}{\variable[Int]{{\color{red}{I}}}}}
}{}{}{}{}
$
\item[] Concrete configuration:\\
\hspace*{5ex}$\kall[blue]{k}{\variable[Pgm]{\texttt{{\color{blue}{i}}={\color{red}{1}}; while(i<=n)\{ S=S+i; i=i+1;\}}}}$\\
\hspace*{5ex}$\mathrel{}\kall[yellow]{state}{\texttt{S} \mapsto 0~{\color{blue}{\texttt{i}}} \mapsto {\color{green}{0}}~\texttt{n} \mapsto 10}$
\end{itemize}
}

\frame{
  \frametitle{IMP semantics}
  \begin{itemize}
\item[] Assignment:\\
\hspace*{10ex}
${
\kprefix[blue]{k}{\reduce{{\variable[K]{X}}\terminal{=}{\variable[Int]{I}}\terminal{;}}{\dotCt{K}}}
\mathrel{}\kmiddle[yellow]{state}{\variable[K]{X}\mapsto\reduce{\AnyVar[K]}{\variable[Int]{I}}}
}{}{}{}{}
$
\item[] Concrete configuration:\\
\hspace*{5ex}$\kall[blue]{k}{\variable[Pgm]{\texttt{while(i<=n)\{ S=S+i; i=i+1;\}}}}$\\
\hspace*{5ex}$\mathrel{}\kall[yellow]{state}{\texttt{S} \mapsto 0~\texttt{i} \mapsto {\color{red}{1}}~\texttt{n} \mapsto 10}$
\end{itemize}
}

\frame{
  \frametitle{Creating Hoare Logic-based verification tools in \K}
  \begin{itemize}
  \item<1-> In practice, a Hoare Logic verifier is language dependent
  \begin{itemize}
    \item<2-> deductive rules depend on the language syntactical constructs
    \item<2-> syntax of the logical assertions %is the same as the language syntax
%    \item<2-> program variables are also logical variables
    \item<2-> ...
  \end{itemize}
  \item<3-> We have to deal with 
  \begin{itemize}
  \item<4->language dependency issues (syntax \& semantics)
  \item<5->support for verification of Hoare triples in \K (transform Hoare triples into Reachability formulas)
  \end{itemize}
%  \item<5-> How can we perform verification of Hoare triples in \K?
%  \begin{itemize}
%    \item<6-> 
%  \end{itemize}
  \end{itemize}
}




\frame{
\frametitle{Hoare Logic vs. Reachability logic - example}
\small
\begin{itemize}
\item<1-> \texttt{SUM} $=$ ``\texttt{S=0; i=1; while(i<=n)\{ S=S+i; i=i+1;\}}"\\~\\
\item<2-> Hoare triple:\\~\\
\hspace{5ex}$\{\mathtt{n} \geq 0\}$ \texttt{SUM} $\{\mathtt{S} = \mathtt{n} * (\mathtt{n} + \mathtt{1}) / 2\}$
\item<3-> Reachability rule:\\~\\
\hspace{5ex}${\kall[blue]{k}{\mathtt{SUM}}\kall[yellow]{state}{\mathtt{S} \mapsto s, \mathtt{n} \mapsto n, \mathtt{i} \mapsto i}}\, \land n \geq 0 \Rightarrow$\\
\hspace{5ex}${\kall[blue]{k}{\mathtt{\kdot}}\kall[yellow]{state}{\mathtt{S} \mapsto s', \mathtt{n} \mapsto n', \mathtt{i} \mapsto i'}} \land s'=n * (n + 1) / \text{ } 2$\\~\\
  \item<4->{
  \begin{thebibliography}{1}
\bibitem{rosu-stefanescu-2012-fm}
Grigore Ro\c{s}u and Andrei \c{S}tef\u{a}nescu.
\newblock From hoare logic to matching logic reachability.
\newblock FM'12
\end{thebibliography}
  }

\end{itemize}
}

%\frame{
%  \frametitle{From Hoare Triples to Reachability Rules}
%  
%  \begin{itemize}
%  \item<1->For IMP, any Hoare triple:
%   $$\htriple{\psi}{Stmt}{\psi'}$$
%    can be encoded as a reachability rule:
%$$(\exists {X}){\kall[black]{k}{Stmt}\kall[black]{state}{\sigma_{X}}}\land\psi_{X,Y} \Rightarrow (\exists{X}){\kall[black]{k}{\kdot}\kall[black]{state}{\sigma_{X}}}\land\psi'_{X,Y}$$
%
%  \item<2->{
%  \begin{thebibliography}{1}
%\bibitem{rosu-stefanescu-2012-fm}
%Grigore Ro\c{s}u and Andrei \c{S}tef\u{a}nescu.
%\newblock From hoare logic to matching logic reachability.
%\newblock FM'12
%\end{thebibliography}
%  }
%  \end{itemize}
%  
%}


%
%\frame{
%  \frametitle{IMP semantics: statements}
%
%\small
%\vspace{2ex}
%\begin{minipage}{.45\linewidth}
%\krule{
%\kprefix[black]{k}{\reduce{{}\terminal{if}({\constant[\#Bool]{true}}){\variable[K]{S}}\terminal{else}{\AnyVar[K]}}{\variable[K]{S}}}
%}{}{}{}{}
%\end{minipage}
%\begin{minipage}{.45\linewidth}
%\krule{
%\kprefix[black]{k}{\reduce{{}\terminal{if}({\constant[\#Bool]{false}}){\AnyVar[K]}\terminal{else}{\variable[K]{S}}}{\variable[K]{S}}}
%}{}{}{}{}
%\end{minipage}
%\vspace{2ex}
%\krule{
%\kprefix[black]{k}{
%\reduce{{}\terminal{while}({\variable[K]{B}}){\variable[K]{S}}}{{}\terminal{if}({\variable[K]{B}}){\{{{\variable[K]{S}}\mathrel{}{{}\terminal{while}({\variable[K]{B}}){\variable[K]{S}}}}\}}\terminal{else}{\{\}}}}}{}{}{}{}
%}

%\section{Symbolic execution in \K}
%\frame{
%  \frametitle{Symbolic execution in \K}
%  \begin{itemize}
%  \item<1-> Given {$\mathcal{S}$}  the \K semantics of {$\mathcal{L}$}
%  \item<1-> The \K tool generates {$\mathcal{S}^\mathfrak{s}$} - the ``symbolic semantics''
%  \item<1-> Using $\mathcal{S}^\mathfrak{s}$ we can execute programs having symbolic inputs
%  \item<1-> Output: a set of constraints corresponding to program paths
%  \item<2-> The transformation of $\mathcal{S}$ into $\mathcal{S}^\mathfrak{s}$ does not affect the initial semantics of $\mathcal{L}$
%  \item<2-> Language independent: the transformation applies to $\mathcal{S}$, not $\mathcal{L}$
%  \item<3->
%  \begin{thebibliography}{1}
%\bibitem{ArusoaieLR2013SLE}
%Andrei Arusoaie, Dorel Lucanu, and Vlad Rusu.
%\newblock A generic framework for symbolic execution.
%\newblock In {\em 6th International Conference on Software Language
%  Engineering}, vol. 8225, {\em LNCS}, p. 281--301. Springer Verlag,
%  2013.
%\end{thebibliography}
%  \end{itemize}
%}
%
%
%\section{Reachability Logic}
%\frame{
%\frametitle{Reachability Logic}
%\begin{itemize}
%\item<1-> Proposed by Grigore Ro\c{s}u as an alternative to Hoare Logic
%\item<1-> Program properties are given as reachability rules:\\
%$$
%\varphi \Rightarrow \varphi',
%$$
%where $\varphi$ and $\varphi'$ are called patterns.
%\item<1-> A pattern $\varphi=\pi\land\psi$, where $\pi$ defines a set of (concrete) configurations and $\psi$ is a first order formula which constrains these configurations
%\end{itemize}
%}
%

\section{Methodology}

\frame{
  \frametitle{Verification of Hoare triples using symbolic execution}
  \begin{itemize}
  \item<1-> Intuition: transform Hoare triples into reachability rules and verify them using symbolic execution
  \item<2-> If $\varphi\Rightarrow\varphi'$, where $\varphi=\pi\land\psi$, then
  \begin{itemize}
   \item<3-> \texttt{assume} $\varphi$: $\pi$ the initial configuration, $\psi$ the initial path condition
   \item<4-> perform symbolic execution of $\varphi$, and obtain $\{\varphi''\}$
   \item<5-> check if for all $\varphi''$, $\varphi''$ \texttt{implies} $\varphi'$
  \end{itemize}
  \end{itemize}
}

%\frame{
%  \frametitle{Symbolic execution in \K}
%  \begin{itemize}
%  \item<1-> Given {$\mathcal{S}$}  the \K semantics of {$\mathcal{L}$}
%  \item<1-> The \K tool generates {$\mathcal{S}^\mathfrak{s}$} - the ``symbolic semantics''
%  \item<1-> Using $\mathcal{S}^\mathfrak{s}$ we can execute programs having symbolic inputs
%  \item<1-> Output: a set of constraints corresponding to program paths
%  \item<2-> The transformation of $\mathcal{S}$ into $\mathcal{S}^\mathfrak{s}$ does not affect the initial semantics of $\mathcal{L}$
%  \item<2-> Language independent: the transformation applies to $\mathcal{S}$, not $\mathcal{L}$
%  \item<3->
%  \begin{thebibliography}{1}
%\bibitem{ArusoaieLR2013SLE}
%Andrei Arusoaie, Dorel Lucanu, and Vlad Rusu.
%\newblock A generic framework for symbolic execution.
%\newblock SLE'13.
%\end{thebibliography}
%  \end{itemize}
%}

\frame{
\frametitle{Methodology}
\begin{itemize}
  \item<1-> Steps:
  \begin{itemize}
     \item<2-> Add syntax and semantics for Hoare-like annotations
     \item<3-> Define \texttt{assume} \& \texttt{implies} operations for checking reachability rules
  \end{itemize}
\end{itemize}
}

\frame{
  \frametitle{Add syntax for Hoare-like annotations}
%\hspace{3ex}\begin{minipage}{\textwidth}
\texttt{
\hspace{-1.3ex}pre: 0 <= n\\
post: 2 * S == n * (n + 1)\\
\vspace{1ex}
S = 0;\\
i = 1;\\
while (i <= n)\\
inv: 2*S == i * (i - 1)  and i <= n + 1\\
\{\\
~\hspace{2ex}S = S + i;\\
~\hspace{2ex}i = i + 1;\\
\}\\
}
%\end{minipage}
}

\frame{
\frametitle{Semantics of the new constructs}
\begin{itemize}
\item Pre/post conditions
\[
%\ax{HT}:\\
\small
\selectfont
\hspace{-4ex}
{
\reduce{\terminal{pre:}\psi\terminal{post:}\psi'\text{ }Stmt}
{\terminal{assume}(\kall[blue]{k}{Stmt}\kall[yellow]{state}{\sigma}\land{\psi})\kra\terminal{implies}(\kall[blue]{k}{\kdot}\kall[yellow]{state}{\sigma'}\land{\psi'})}}
%\kall[black]{state}{\AnyVar}
%\kall[black]{cond}{\AnyVar}
\]
\end{itemize}
}

\frame{
\frametitle{Semantics of the new constructs}
\begin{itemize}
\item \texttt{while} loop
\[
\small
\selectfont
\hspace{-4ex}
{\reduce{\mathtt{while}({\it B}){\terminal{inv:}}\psi\;Stmt\kra K}
{{\terminal{assume}}(\kall[blue]{k}{Stmt}\kall[yellow]{state}{\sigma}\land{B \land \psi})\!\kra\!{\terminal{implies}}(\kall[blue]{k}{\kdot}\kall[yellow]{state}{\sigma'}\land{\psi})
}}
\]
\[
\small
\selectfont
\hspace{-4ex}
{\reduce{\mathtt{while}({\it B}){\terminal{inv:}}\psi\;Stmt\kra K}{
{\terminal{implies}}(\kall[blue]{k}{\kdot}\kall[yellow]{state}{\hspace{-1em}\sigma'\hspace{-1em}}\land{\psi})\!\kra\!
{\terminal{assume}}(\kall[blue]{k}{K}\kall[yellow]{state}{\sigma}\land{\neg B \land \psi})}}
\]
\end{itemize}
}

\frame{
  \frametitle{Define \texttt{assume}}
  \begin{itemize}
  \item \texttt{assume} semantics:\\~\\
  \noindent\[
\fontsize{9}{11}
\selectfont
\kprefix[white]{k}{\reduce{\terminal{assume}({\kall[blue]{k}{Stmt}\kall[yellow]{state}{E}\land{\psi})}}{Stmt}}
\kall[white]{state}{\reduce{\AnyVar}{E}}\land{\reduce{\AnyVar}{\psi}}\vspace{-1ex}
\]
\end{itemize}
}

\frame{
  \frametitle{Define \texttt{implies}}
  \begin{itemize}
 \item \texttt{implies} semantics:\\~\\
 $\fontsize{9}{11}
\selectfont
\hspace{5ex}\kall[white]{k}{\reduce{\terminal{implies}({\kall[blue]{k}{\kdot}\kall[yellow]{state}{E'}\land{\psi'}})}{\kdot}}
\kall[white]{state}{E''}\land{\psi''}$\\
\hspace{15ex}$\mathtt{when}\text{ }
({\kall[yellow]{state}{E''}\land{\psi''}}) \rightarrow ({\kall[yellow]{state}{E'}\land{\psi'}})
%{\mathit unsat}(\psi'' 
%\land \bigwedge_{\sigma''} 
%\land \neg(\psi'
% \land \bigwedge_{\sigma'}
%))
$
  \end{itemize}
}

%\frame{
%  \frametitle{Add syntax for Hoare-like annotations}
%%\hspace{3ex}\begin{minipage}{\textwidth}
%If we consider the following macros:\\
%\hspace{1cm}\texttt{BODY} $=$ \texttt{S = S + i; i = i + 1;}\\
%\hspace{1cm}\texttt{INV}\hspace{2ex}$=$ \texttt{2*S == i * (i - 1)  and i <= n + 1}\\
%\hspace{1cm}\texttt{LOOP} $=$ \texttt{while(i$\leq$n) inv: INV \{ BODY \} }\\
%then:\\
%
%$
%%\fontsize{9}{11}
%%\selectfont
%%\hspace{-1ex}
%%\kall[black]{k}{\reduce{\mathtt{while(i \leq n)~inv:~INV~\{ BODY \} }\kra K}
%%{{\terminal{assume}}(\kall[black]{k}{\mathtt{BODY}}\kall[black]{state}{\mathtt{S} \mapsto s~\mathtt{n} \mapsto n~\mathtt{i} \mapsto i}\land (i \leq n) \land \psi \land s = 0 \land i = 1)\\\kra\!{\terminal{implies}}(\kall[black]{k}{\kdot}\kall[black]{state}{\mathtt{S} \mapsto s'~\mathtt{n} \mapsto n'~\mathtt{i} \mapsto i'}\kall[black]{cond}{\psi})
%%}}
%$
%
%
%
%}


%\frame{
%\frametitle{\texttt{while}}
%\small
%Let us consider the following code macros:\\
%\hspace{1cm}\texttt{BODY} $=$ \texttt{S = S + i; i = i + 1;}\\
%\hspace{1cm}\texttt{INV}\hspace{2ex}$=$ \texttt{2*S == i * (i - 1)  and i <= n + 1}\\
%\hspace{1cm}\texttt{SUM} $=$ \texttt{S=0; i=1; while(i$\leq$n) inv: INV \{ BODY \} }\\~\\
%
%
%{$\mathtt{while(i \leq n)~inv:~INV~\{ BODY \} }\kra K$}
%  \begin{itemize}
%  \item ${\terminal{assume}}(\kall[black]{k}{\mathtt{BODY}}\kall[black]{state}{\mathtt{S} \mapsto s~\mathtt{n} \mapsto n~\mathtt{i} \mapsto i} \land (i \leq n \land s = 0 \land i = 1)$\\
%  $\kra {\terminal{implies}}(\kall[black]{k}{\kdot}\kall[black]{state}{\mathtt{S} \mapsto s'~\mathtt{n} \mapsto n'~\mathtt{i} \mapsto i'}\kall[black]{cond}{\psi})$
%  \end{itemize}
%}

%\section{Evaluation}
%\frame{
%\frametitle{Evaluation}
%\begin{itemize}
%\item Using our methodology we created IMP-Hoare
%\item We tested it against KeY-Hoare tests suite
%\end{itemize}
%\begin{table}
%\small
%\renewcommand\thetable{I}
%\centering
%\begin{tabular}{| l | c | c | c |}
%\hline
%\hline
%Programs & IMP-Hoare & Key-Hoare & Spec\#\\
%% & verif. time (sec.) &  verif. time (sec.) \\ 
%\hline\hline
%%\hline
%\texttt{arraySort}&3.98&0.90&4.40\\
%\texttt{arraySwap}&2.78&0.10&3.17\\
%\texttt{countdown}&3.06&0.10&2.57\\
%\texttt{countdownExecutionTime}&2.83&0.10&2.63\\
%\texttt{countdownTotal}&2.87&0.10&2.13\\
%\texttt{delta\_solutions}&3.25&0.10&3.05\\
%\texttt{gcd}&3.13&0.30&2.82\\
%\texttt{integer\_division}&3.70&0.20&3.45\\
%\texttt{max}&2.82&0.02&2.80\\
%\texttt{multiplication}&3.35&0.20&3.12\\
%\hline\hline
%\end{tabular}
%\end{table}
%}

%\frame{
%  \frametitle{Evaluation}
%  \begin{itemize}
%  \item KeY-Hoare is faster
%  \item ... However, it is not very scalable
%  \item Our methodology 
%  \end{itemize}
%}

\section{Conclusions}
\frame{
  \frametitle{Conclusions}
  \begin{itemize}
  \item<1-> Methodology to create a Hoare Logic verifier in \K
  \item<2-> Prove reachability rules generated from Hoare triples, using symbolic execution
  \item<3-> Future work: eliminate \texttt{assume} and \texttt{implies}
%  \item<4-> Apply this methodology on real-life languages
  \end{itemize}
}

\frame{
\frametitle{Thank you!}
The \K framework webpage:
\begin{center}
\url{http://kframework.org/}
\end{center}
}

\bibliographystyle{plain}
%\bibliography{paper}


\end{document}
